g:IMonoid, n:, e:|g|. n x(*;e) e  |g| 

latex

Up	groups 1
Definitions of Statement	IMonoid, n x(op;id) e
Definitions	x. t(x), n x(op;id) e, t  T, x:A. B(x), x(s), , IMonoid
Lemmas	imon wf, nat wf, int seg wf, grp id wf, grp op wf, grp car wf, itop wf